Curry–Howard Correspondence

释义 Definition

Curry–Howard correspondence（柯里—霍华德对应）：逻辑与计算之间的一种深刻对应关系，通常概括为：命题对应类型（propositions-as-types）、证明对应程序（proofs-as-programs）。它是类型论、函数式编程与证明助手（如 Coq、Agda）背后的重要思想。（在一些语境中也常称 Curry–Howard isomorphism。）

发音 Pronunciation (IPA)

/ˈkʌri ˈhaʊərd ˌkɔrəˈspɑndəns/

词源 Etymology

该术语以两位学者命名：Haskell Curry（哈斯凯尔·柯里）与 William Alvin Howard（威廉·阿尔文·霍华德）。Curry 的工作与组合子逻辑、类型化体系相关；Howard 在 1969 年的手稿中系统阐述了“证明 = 程序”这类对应观点。correspondence 意为“对应关系”。

例句 Examples

The Curry–Howard correspondence links logical proofs to computer programs.
柯里—霍华德对应把逻辑证明与计算机程序联系起来。

Under the Curry–Howard correspondence, a function of type A → B can be seen as a proof that A implies B, which guides the design of typed functional languages.
在柯里—霍华德对应下，类型为 A → B 的函数可视为“A 蕴含 B”的一个证明，这也影响了类型化函数式语言的设计。

相关词 Related Words

• Isomorphism
• Type Theory
• Lambda Calculus
• Proposition
• Proof
• Functional Programming
• Dependent Type
• Proof Assistant

文学与著作 Literary Works

• Howard, W. A. (1969). The formulae-as-types notion of construction（提出“公式即类型/证明即程序”的经典手稿，后广为引用）。
• Sørensen, M. H., & Urzyczyn, P. Lectures on the Curry–Howard Isomorphism（系统教材，详细讲解该对应及其变体）。
• Wadler, P. (2015). Propositions as Types（面向程序语言读者的经典文章，普及“命题即类型”）。
• Pierce, B. C. Types and Programming Languages（多处讨论类型系统与逻辑之间的联系，常提及该对应思想）。